%!TEX root = /Users/adriaan/src/kinded-scala/papers/oopsla/tcpoly.tex

\lstdefinelanguage{scalina}{% 
       morekeywords={% 
                type, val, new, Un, In, Struct, Nominal, Concrete, *, Any, Nothing},% 
         sensitive=t, % 
   morecomment=[s]{/*}{*/},morecomment=[l]{\//},% 
   escapeinside={/*\%}{*/},%
   rangeprefix= /*< ,rangesuffix= >*/,%
   morestring=[d]{"}% 
 }
 
\section{Object-Oriented Formalism \label{sec:scalina}}
This section outlines the foundations of our extension by translating a subset of Scala into a formally defined object-oriented calculus. It does not introduce any new features, and it may thus be skipped on first reading. Moreover, as discussed in Section \ref{sec:related}, many others have worked out the formal intricacies that underlie our extension; we focus on bringing them together in a full-blown, object-oriented, language.

\subsection{Introduction}
We use Scalina, which we presented in detail in earlier work \cite{moors08:scalina}, as a model for Scala. Scalina is a simplification of the \nuObj~calculus \cite{DBLP:conf/ecoop/OderskyCRZ03}, extended with one crucial feature: un-members. Whereas normal members behave covariantly -- and as such, they are suited to encode the result of a function -- un-members introduce \emph{contravariance}, so that they can be used to encode parameters. In other words, normal members represent output from an abstraction to its clients, while un-members are used for input, like the arguments of a method or a class's type parameters.


\begin{figure}
  \centering
    \includegraphics[width=\columnwidth]{scalina_terms_types}
  \caption{Scalina syntax for terms, types, and members}
  \label{fig:types}
\end{figure}

Scalina is a three-level calculus. Kinds classify types, which in turn classify values. Figure \ref{fig:types} defines the syntax for its types and values. A value, an object, may have concrete value or type members, and value or type un-members. An un-member is turned into a concrete member using member refinement. 
Syntactically, an un-member is distinguished from an abstract member by its classifier, which is either \type{Un[TT]} or \type{Un[KK]}.

The remaining value-level operations are instantiation, which is only allowed on types without abstract members (i.e., only concrete ones or un-members), and
value member selection, which is not allowed on objects with un-members (they must first be provided using refinement).

The level of types consists of the standard structural types, singleton types, intersection types, and type member selection. We supplement this with type member refinement, which, analogously to the value level, turns a type un-member into a concrete type member by supplying its right-hand side. Finally, the un-type constructor turns a type into an un-type, which is not inhabited. Thus, \type{Un[TT]} is used to classify a value un-member that can be refined to a concrete value member with type \type{TT}.

The typing and kinding rules, which have been included in the appendix, are as expected, with the necessary caveat due to the introduction of un-members. Subsumption may be used by clients to relax their expectations of an abstraction, but it would be unsound to also allow a client to relax its \emph{obligations} towards the abstraction. Thus, un-members represent an exception to the usual width-subtyping rule for structural types, as a client should not be able to forget them using subsumption. Correspondingly, a type member's bounds must not be strengthened by a subtype, that is, they behave contravariantly.

Finally, as shown in Fig. \ref{fig:kinds}, Scalina uses kinds to uniformly support bounded type members (through the interval kind), structural types, nominal subtyping, and type un-members. The \kind{Concrete} kind captures types that may be instantiated.


\begin{figure}
  \centering
    \includegraphics[width=\columnwidth]{scalina_kinds}
  \caption{Scalina syntax for kinds, paths, and values}
  \label{fig:kinds}
\end{figure}

\subsection{Encoding \label{sec:encoding}}
We illustrate the encoding from Scala into Scalina using a series of examples. We set out with the smallest Scala program that we are interested in:

\begin{lstlisting}[frame=no]
class List[T]  
\end{lstlisting}

In Scalina, a class is modelled as a type member, which is necessarily nested in another type. We call the root of this nesting hierarchy, a plain object, the ``universe'', which is reflected by the name of its self variable, \code{u}. More precisely, a type member that encodes a class, is an alias for the intersection type that composes the class's parents (if any) with its body. To indicate that nominal subtyping should be used to determine whether a type is a subtype of this type member, it receives the kind \kind{Nominal(R)}, where \type{R} roughly corresponds to the (structural) flattening of the member's right-hand side. 

Type parameters are turned into type un-members (which are distinct from \emph{abstract} members!). \type{T}'s implicit lower and upper bounds are made explicit using the interval kind \kind{In(Nothing, Any)}, which we again abbreviate as \kind{*}. 

% omitted from List, since not needed in example: `this : []u.type#List`
\begin{lstlisting}[language=scalina,frame=no]
new { u =>
 type List: Nominal({type T: Un[*]})={this =>
   type T: Un[*] 
 }
}
\end{lstlisting}

Thus, the following Scalina type encodes the Scala type \type{List[Int]}:

\begin{lstlisting}[language=scalina,frame=no]
u.type#List<{type T = Int}
\end{lstlisting}

Since type members may only be selected on types, we turn the universe object's self variable into the singleton type that is only inhabited by that object. Then, the \type{List} type member is selected, and the type un-member that represents its first type parameter is turned into the corresponding concrete type member that is equal to \type{Int}, which is assumed to be built-in.


To illustrate the higher-kinded case, consider:

\begin{lstlisting}[frame=no]
class Builder[Container[X]]  
\end{lstlisting}

We transform this into a Scalina-style type member definition, while abbreviating the pattern \code{type C : Nominal(R) = T} to \code{type C <~ T}, as the omitted information can be inferred.

\begin{lstlisting}[language=scalina,frame=no]
  type Builder <~ { this =>
    type Container: Un[Struct({type X: Un[*]; type Apply: *})]
  }
\end{lstlisting}

Here, the interesting bit is how we abstract over a type constructor of kind \kind{* -> *}: this corresponds precisely to a structural type with a type un-member for the higher-order type parameter, and an abstract type member \type{Apply} to retrieve the type function's result. This encoding is similar to the encoding of functions in \nuObj, except that we can now correctly use an un-member for the encoding of a parameter. Note that bounds on the higher-order type parameter \type{X} can easily be encoded as the kind of the \type{X} un-member, and similarly for the \type{Container} parameter: its bounds determine the kind of the \type{Apply} member. 

Note that the previous scheme for type applications needs to be adapted slightly when an abstract type constructor is involved. In the context of the class \type{Builder}, a type application such as \type{Container[Int]} is written as:

\begin{lstlisting}[language=scalina,frame=no]
(this.type#Container<{type X = Int})#Apply
\end{lstlisting}

The type \type{Builder[List]} becomes:

\begin{lstlisting}[language=scalina,frame=no]
u.type#Builder<{type Container = 
  {s : {type X: *} =>
    type X: Un[*]; 
    type Apply: * =
      u.type#List<{type T=s.type#X}}}     
\end{lstlisting}

Finally, an algorithm for this encoding should use a naming scheme that codifies the positional nature and the class-local scope of type parameters. We do not discuss this as it does not affect correctness, nor does it provide any new insights.

\subsection{Soundness}
In this context, kind preservation is the property that a well-kinded type normalises to a type with the same kind, modulo kind subsumption. Kind progress states that a well-kinded type is either a canonical type, or it can be normalised to one. Together, these properties imply kind soundness. As type normalisation corresponds to evaluation, and kinding is the equivalent of typing, the analogy with type soundness should be clear.

% TODO: which types are canonical? :-s

Together with the encoding, the kinding and typing rules from the appendix form a precise specification of the relevant checks in the Scala compiler. Thus, soundness of Scalina carries over to the fragment of Scala that Scalina encodes. Variance is the only missing feature, as discussed in Section \ref{sec:variance}. Finally, Scalina is intended as a minimal object-oriented calculus with features that exceed the needs of the current paper, as motivated in earlier work \cite{moors08:scalina}. Its development is ongoing work, including more powerful support for type-level computation, and a mechanisation of its meta-theory.